Nuprl Lemma : equal-nil-lists
0,22
postcript
pdf
T
:Type,
x
,
y
:Top List. null(
x
)
null(
y
)
x
=
y
T
List
latex
Definitions
False
,
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
,
True
,
type
List
,
nil
,
b
,
Top
,
x
:
A
B
(
x
)
,
s
=
t
,
Type
Lemmas
top
wf
,
true
wf
,
false
wf
origin